Thank you for the detailed analysis. Updated. PTAL.

It specifies that the flow model M after the for statement is join(false(C), unsplit(break(S)) where we have taken the 'types of interest' for each variable in after(U) and added to the types of interest for the same variable in M (and skipped variables in after(U) that aren't in M).

It's an interesting about type of interest. It can be tested (in a separate PR).

class S {}
class T extends S {
  void foo() {}
}

test1() {
  S s = S();
  for (;false;) {
    if (s is T) {} // make `T` a  type of interest
  }
  s = T();
  s.foo(); // Not an error.
}

test2() {
  S s = S();
  for (;false; s is T) {
  }
  s = T();
  s.foo(); // Error. Not an issue, result of the conservativeJoin()? Same as https://github.com/dart-lang/sdk/issues/60320 ?
}

Is this an expected that there is an error in test2()?

The for statement rule actually justifies that S is unreachable: before(S) = split(true(C)) and true(C) is unreachable. So after(S) would also be unreachable, and so is continue(S) (because there are no continue; statements). So before(U) is unreachable, and hence U (that is s is T) is dead code.

This justifies the error at the end, in the line with a long comment.

The for statement rule actually justifies that S is unreachable: before(S) = split(true(C)) and true(C) is unreachable. So after(S) would also be unreachable, and so is continue(S) (because there are no continue; statements). So before(U) is unreachable, and hence U (that is s is T) is dead code.

This justifies the error at the end, in the line with a long comment.

After the testing and rereading the spec I think that there is another reason of such behavior. According to the spec:

We say that at type T is a type of interest for a variable x in a set of tested types tested if tested contains a type S such that T is S, or T is NonNull(S).

Definition of tested is:

tested is a set of types which are considered "of interest" for the purposes of promotion, generally because the variable in question has been tested against the type on some path in some way.

I think it is too general definition but the key point here is "for the purposes of promotion". So s is T itself doesn't promote anything. Therefore:

s = S();
s is T;
s = T();
s.foo(); // Error. There were no promotion above

And for the same reason we are getting an error in case of for (;false; s is T).... To get the promoution we should do something like:

  S s = S();
  int i = 0;
  for (;false; s is T ? i++ : i += 2) {}
  s = T();
  s.foo();  // Ok, now accepted

Please correct me the above is wrong. Otherwise it'd be nice to test type of interest in all of the places where we should have a promotion.

• instance check If N is an expression of the form E1 is S where the static type of E1 is T then:
  ...
  Otherwise:
• Let true(N) = promote(E1, S, after(E1))
• Let false(N) = promote(E1, factor(T, S), after(E1))

As far as I understand to get a promotion after the type check we should have true(N) or false(N) branch (in case of plain s is T; the both branches are empty that's why we have no promotion). But we have the promotion, for example, in the following case:

s = S();
s is T && 2 > 1; // `true(N)` branch added to `s is T`
s = T();
s.foo(); // Now Ok!

So to test types of interest we should check all of the places in the flow analysys spec where true(N), false(N) or promote() occurs. s = T(); s.foo(); shouldn't produce an error after it.

Please correct me if I'm wrong.

So s is T itself doesn't promote anything

The flow models associated with the evaluation of the expression s is T do not agree, but both true(N) and false(N) may have a 'promoted' stack for s which reflects the newly obtained information about the run-time type of s.

I do think it's fair to say that "s is T can promote s in the true continuation or the false continuation, or both". Of course, it also adds T to the set of tested types for s.

s = S();
s is T;
s = T();
s.foo(); // Error. There were no promotion above

That's a bug! The flow model after(N) where N is the node that contains s is T should be obtained as join(true(N), false(N)), and the true(N) flow model should consider T to be a type of interest for s. The factor function might makes some other type a type of interest for s as well, but that wouldn't invalidate the fact that T is of interest in subsequent code.

Given that T is a type of interest when s = T() is reached, this assignment should promote s to T.

It has probably never been reported because it is a pointless statement: We're computing a boolean value and discarding it, and there are no side effects. In any case, I do believe that this is a bug.

To get the promoution we should do something like:

 S s = S();
 int i = 0;
 for (;false; s is T ? i++ : i += 2) {}
 s = T();
 s.foo();  // Ok, now accepted

In this case the type test s is T is again in dead code, but this is not discovered during the inheritTested step, so T is considered to be a type of interest for s when we reach s = T();, which will then promote s to have type T.

As far as I understand to get a promotion after the type check we should have true(N) or false(N) branch (in case of plain s is T; the both branches are empty that's why we have no promotion).

No, the point is that the true and false branches are joined, it wouldn't make a difference if one or both of those branches had some code in them (as long as that code doesn't interfere with the status of s in some other way, and as long as the branches aren't unreachable).

s = S();
s is T && 2 > 1;
s = T();
s.foo(); // Now Ok!

Looks like the bug that came up above doesn't apply here, probably because the true continuation is needed for the flow analysis of the rest of the expression.

@stereotype441, do you agree that the following is a bug?:

class S {}

class T extends S {
  void foo() {}
}

void main() {
  var s = S();
  s is T;
  s = T();
  s.foo(); // Error, so `T` was not a type of interest, but it should be.
}

@eernstg

@stereotype441, do you agree that the following is a bug?:

class S {}

class T extends S {
  void foo() {}
}

void main() {
  var s = S();
  s is T;
  s = T();
  s.foo(); // Error, so `T` was not a type of interest, but it should be.
}

Yes, good catch! I've filed dart-lang/sdk#60479 to track it. And nice job with the analysis above; I walked through the code in the debugger and confirmed that what's happening is exactly what you surmised.